//package useless;
//
//import atom.UnaryAtom;
//import formula.BinaryFormula;
//import formula.UnaryFormula;
//import literal.UnaryLiteral;
//import proof.ConclusionProof;
//import proof.Proof;
//import sign.FormulaSign;
//
//import java.util.ArrayList;
//import java.util.Random;
//
//public class GF3 {//生成3个formulas
//    public ArrayList<String> getElement(){
//        String[] alphabet={"a","b","c","d","e","f","g","h","i","j","k","l","m","n",
//                "o","p","q","r","s","t","u","v","w","x","y","z"};
//        ArrayList<String> arr=new ArrayList<>();
//        for (int i = 0; i < 5; i++) {//在alphabet中挑选5个字母作为初始输入
//            Random random=new Random();
//            int randomInt=random.nextInt(26);
//            String atom=alphabet[randomInt];
//            arr.add(atom);
//        }
////        for (String str:arr) {
////            System.out.println(str);
////        }
//        return arr;
//    }
//
//    public UnaryFormula getAtom(ArrayList<UnaryFormula> ufArr1,ArrayList<UnaryFormula> ufArr2){//uf1是atom的list，uf2是not atom的list
//        //70%概率选择atom（false），30%选择not atom（true，即带负号）
//        //返回值是一个被选中的uf
//        Random random = new Random();
//        double randomValue = random.nextDouble();
//        if (randomValue<0.7){//此时从ufArr1中挑选1个atom
//            int index = random.nextInt(5);//同15行选中的初始字母数量
//            return ufArr1.get(index);
//        }else {//此时从ufArr2中挑选1个atom
//            int index = random.nextInt(5);//同15行选中的初始字母数量
//            return ufArr2.get(index);
//        }
//    }
//
//    public BinaryFormula generateBF(ArrayList<String> arr){
//        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
//        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
//        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
//        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
//        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
//        ArrayList<UnaryFormula> ufArr1=new ArrayList<>();
//        ufArr1.add(uf1);
//        ufArr1.add(uf2);
//        ufArr1.add(uf3);
//        ufArr1.add(uf4);
//        ufArr1.add(uf5);
//
//        UnaryFormula uf6=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),true));
//        UnaryFormula uf7=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),true));
//        UnaryFormula uf8=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),true));
//        UnaryFormula uf9=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),true));
//        UnaryFormula uf10=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),true));
//        ArrayList<UnaryFormula> ufArr2=new ArrayList<>();
//        ufArr2.add(uf6);
//        ufArr2.add(uf7);
//        ufArr2.add(uf8);
//        ufArr2.add(uf9);
//        ufArr2.add(uf10);
//
//        Random randomS=new Random();
//        int sign=randomS.nextInt(2);//random sign
//        if (sign==0){//exist
//            //System.out.println("exist");
//            BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//            return bf;
//        }else{//any
//            //System.out.println("any");
//            BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//            return bf;
//        }
//    }
//
//    public BinaryFormula generateTF(ArrayList<String> arr){//tf (Exist(a,Exist(b,c)))  c 形如uf，但表示ba
//        //ua+ua+ba
//        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
//        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
//        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
//        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
//        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
//        ArrayList<UnaryFormula> ufArr1=new ArrayList<>();
//        ufArr1.add(uf1);
//        ufArr1.add(uf2);
//        ufArr1.add(uf3);
//        ufArr1.add(uf4);
//        ufArr1.add(uf5);
//
//        UnaryFormula uf6=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),true));
//        UnaryFormula uf7=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),true));
//        UnaryFormula uf8=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),true));
//        UnaryFormula uf9=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),true));
//        UnaryFormula uf10=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),true));
//        ArrayList<UnaryFormula> ufArr2=new ArrayList<>();
//        ufArr2.add(uf6);
//        ufArr2.add(uf7);
//        ufArr2.add(uf8);
//        ufArr2.add(uf9);
//        ufArr2.add(uf10);
//
//        Random randomS=new Random();
//        int sign=randomS.nextInt(2);//random sign
//        Random randomS2=new Random();
//        int sign2=randomS2.nextInt(2);//random sign(inner one)
//
//        if (sign==0){//outer sign is exist
//            if (sign2==0){//inner sign is exist
//                //total formula is (E,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (E,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }else {//outer sign is for all
//            if (sign2==0){//inner sign is exist
//                //total formula is (A,E)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }else{//inner sign is for any
//                //total formula is (A,A)
//                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),getAtom(ufArr1,ufArr2));
//                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,getAtom(ufArr1,ufArr2),bfInner);
//                return bf;
//            }
//        }
//    }
//
//    public BinaryFormula generateConclusion(ArrayList<String> arr){
//        Random random=new Random();
//        int flag= random.nextInt(2);
//        if (flag==0){//生成bf
//            return generateBF(arr);
//        }else {//生成tf
//            return generateTF(arr);
//        }
//    }
//
//    public ArrayList<Proof> typeChange(ArrayList<BinaryFormula> conditions){
//        //接收formula，转换成proof
//        ArrayList<Proof> proofs=new ArrayList<>();
//        Proof p1=new ConclusionProof(conditions.get(0));
//        Proof p2=new ConclusionProof(conditions.get(1));
//        Proof p3=new ConclusionProof(conditions.get(2));
////        Proof p4=new ConclusionProof(conditions.get(3));
////        Proof p5=new ConclusionProof(conditions.get(4));
//        proofs.add(p1);
//        proofs.add(p2);
//        proofs.add(p3);
////        proofs.add(p4);
////        proofs.add(p5);
//
//        return proofs;
//
//    }
//
//    public boolean show(ArrayList<Proof> proofs,BinaryFormula conclusion){
//        if (Solve.solveHelper(proofs,conclusion, new UsedCondition())!=null){
//            return true;
//        }else {
//            return false;
//        }
//    }
//
//    public ArrayList<BinaryFormula> bf0(ArrayList<String> arr){//0 bf+3 tf
//        ArrayList<BinaryFormula> bfs=new ArrayList<>();//bfs来存储conditions
//        for (int i = 0; i < 3; i++) {//3 tf
//            BinaryFormula tf=generateTF(arr);
//            bfs.add(tf);
//        }
//        return bfs;
//    }
//
//    public ArrayList<BinaryFormula> bf1(ArrayList<String> arr){//1 bf+2 tf
//        ArrayList<BinaryFormula> bfs=new ArrayList<>();//bfs来存储conditions
//        BinaryFormula bf=generateBF(arr);
//        bfs.add(bf);//1 bf
//        for (int i = 0; i < 2; i++) {//2 tf
//            BinaryFormula tf=generateTF(arr);
//            bfs.add(tf);
//        }
//        return bfs;
//    }
//
//    public ArrayList<BinaryFormula> bf2(ArrayList<String> arr){//2 bf+1 tf
//        ArrayList<BinaryFormula> bfs=new ArrayList<>();//bfs来存储conditions
//        BinaryFormula bf1=generateBF(arr);
//        bfs.add(bf1);
//        BinaryFormula bf2=generateBF(arr);
//        bfs.add(bf2);//2 bf
//        BinaryFormula tf=generateTF(arr);
//        bfs.add(tf);
//
//        return bfs;
//    }
//
//    public ArrayList<BinaryFormula> bf3(ArrayList<String> arr){//3 bf+0 tf
//        ArrayList<BinaryFormula> bfs=new ArrayList<>();//bfs来存储conditions
//        BinaryFormula bf1=generateBF(arr);
//        bfs.add(bf1);
//        BinaryFormula bf2=generateBF(arr);
//        bfs.add(bf2);
//        BinaryFormula bf3=generateBF(arr);
//        bfs.add(bf3);//3 bf
//
//        return bfs;
//    }
//
//    public boolean run(int input){
//        ArrayList<String> arr=getElement();
//        BinaryFormula conclusion=generateConclusion(arr);
//        if (input==0){//bf0+tf3
//            ArrayList<BinaryFormula> conditions=bf0(arr);
//            ArrayList<Proof> proofs=typeChange(conditions);
//            boolean flag=show(proofs,conclusion);
//            if (flag){
//                return true;
//            }else {return false;}
//        }else if (input==1){//bf1+tf2
//            ArrayList<BinaryFormula> conditions=bf1(arr);
//            ArrayList<Proof> proofs=typeChange(conditions);
//            boolean flag=show(proofs,conclusion);
//            if (flag){
//                return true;
//            }else {return false;}
//        }
//        else if (input==2){//bf2+tf1
//            ArrayList<BinaryFormula> conditions=bf2(arr);
//            ArrayList<Proof> proofs=typeChange(conditions);
//            boolean flag=show(proofs,conclusion);
//            if (flag){
//                return true;
//            }else {return false;}
//        }
//        else if (input==3){//bf3+tf0
//            ArrayList<BinaryFormula> conditions=bf3(arr);
//            ArrayList<Proof> proofs=typeChange(conditions);
//            boolean flag=show(proofs,conclusion);
//            if (flag){
//                return true;
//            }else {return false;}
//        } else {
//            return false;
//        }
//    }
//
//
//    public static void main(String[] args) {
//        GF3 gf=new GF3();
////        ArrayList<String>arr=gf.getElement();
////        System.out.println(arr);
////        ArrayList<BinaryFormula> conditions=gf.bf2(arr);
////        System.out.println(conditions);
////        ArrayList<Proof> proofs=gf.typeChange(conditions);
////        System.out.println(proofs);
////        BinaryFormula conclusion=gf.generateConclusion(arr);
////        System.out.println(conclusion);
////        System.out.println(Solve.solveHelper(proofs,conclusion, new UsedCondition()));
//
//        //System.out.println(gf.run(2));
//        float count=0;
//        for (int i=0;i<100;i++){
//            if (gf.run(2)){
//                count=count+1;
//            }
//        }
//        System.out.println("done");
//        System.out.println(count);
//        float probability=(count/100)*100;//概率的百分比
//        String formatted = String.format("%.2f", probability);
//        //System.out.println(probability);
//        System.out.println("P="+formatted+"%");
//
//
//
//    }
//}
